/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓CS258␈↓ ε⊃PROBLEM SET␈↓ 
;WINTER 1979


␈↓ α∧␈↓1. Define

␈↓ α∧␈↓␈↓ αT␈↓↓flat[x,u] ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x.u ␈↓αelse␈↓↓ flat[␈↓αa␈↓↓ x,flat[␈↓αd␈↓↓ x, u]]␈↓.

␈↓ α∧␈↓Prove that ␈↓↓flat␈↓ is total.

␈↓ α∧␈↓2. Prove the termination of the 91-function defined by

␈↓ α∧␈↓␈↓ αT␈↓↓f n ← ␈↓αif␈↓↓ n greater 100 ␈↓αthen␈↓↓ n-10 else f(f(n + 11)␈↓.

␈↓ α∧␈↓3.␈α∂␈↓↓fix␈α∂e␈↓␈α∂is␈α⊂an␈α∂algorithm␈α∂to␈α∂transform␈α∂a␈α⊂compound␈α∂conditional␈α∂expression␈α∂␈↓↓e␈↓␈α∂into␈α⊂an␈α∂equivalent
␈↓ α∧␈↓conditional␈αexpression␈αthat␈αhas␈αonly␈αatomic␈α
propositional␈αparts␈αin␈αthe␈αexpression␈αas␈αa␈α
whole␈αand
␈↓ α∧␈↓its subexpressions.  It uses the rule

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓αif␈↓↓ (␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r) ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ (␈↓αif␈↓↓ q ␈↓αelse␈↓↓ a ␈↓αelse␈↓↓ b) ␈↓αelse␈↓↓ (␈↓αif␈↓↓ r ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b)␈↓

␈↓ α∧␈↓as␈α
long␈α
as␈α
it␈α
is␈α
applicable.␈α
 It␈α
uses␈α
the␈α
abstract␈α
syntax␈α
of␈α
conditional␈α
expressions␈α
which␈αsatisfies␈α
the
␈↓ α∧␈↓following equations:

␈↓ α∧␈↓␈↓ αT␈↓↓prop("if p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b") = "p"

␈↓ α∧␈↓␈↓ αT␈↓↓antec("if p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b") = "a"

␈↓ α∧␈↓␈↓ αT␈↓↓conseq("if p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b") = "c"

␈↓ α∧␈↓␈↓ αT␈↓↓mkcond("p","a","b") = "␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b".

␈↓ α∧␈↓Write␈α⊂the␈α∂algebraic␈α⊂axioms␈α∂and␈α⊂the␈α∂induction␈α⊂schema␈α∂satisfied␈α⊂by␈α∂the␈α⊂functions␈α⊂␈↓↓prop,␈↓␈α∂␈↓↓antec,␈↓
␈↓ α∧␈↓␈↓↓conseq␈↓ and ␈↓↓mkcond␈↓.

␈↓ α∧␈↓Prove the termination of the algorithm ␈↓↓fix␈↓ by inventing a suitable rank function.

␈↓ α∧␈↓␈↓ αT␈↓↓fix␈αe␈α←␈α␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈αe␈α␈↓αthen␈↓↓␈αe␈α␈↓αelse␈↓↓␈α{fix␈αantec␈αe,␈αfix␈αconseq␈αe}␈α[λa␈αb.␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈αprop␈αe␈α␈↓αthen␈↓↓␈αmkcond(prop␈α
e,
␈↓ α∧␈↓↓a, b) ␈↓αelse␈↓↓ fix mkcond(prop prop e, mkcond(antec prop e, a, b), mkcond(conseq prop e, a, b))]␈↓.

␈↓ α∧␈↓4.␈αA␈αterm␈α␈↓↓t␈↓␈αmay␈αbe␈αsubstituted␈αfor␈αa␈αvariable␈α␈↓↓x␈↓␈αin␈αan␈αexpression␈α␈↓↓e␈↓␈αprovided␈αno␈αvariable␈αfree␈αin␈α␈↓↓t␈↓
␈↓ α∧␈↓will␈αbe␈αcaptured␈αby␈αa␈αquantifier␈αin␈α␈↓↓e.␈↓␈αSuppose␈αthat␈αthe␈αexpressions␈αare␈αin␈αLisp␈αform␈αand␈αthat␈α
the
␈↓ α∧␈↓only␈αquantifiers␈αare␈α∀,␈α∃␈αand␈αλ,␈αused␈αin␈αthe␈αforms␈α(∀␈α<varlist>␈α<wff>),␈α(∃␈α<varlist>␈α<wff>)␈αand␈α(λ
␈↓ α∧␈↓<varlist>␈α<term>),␈αwrite␈αthe␈αLisp␈αpredicate␈α␈↓↓freefor[x,t,e]␈↓␈αand␈αprove␈αthat␈αit␈αis␈αtotal.␈α Prove␈αthat␈αif
␈↓ α∧␈↓␈↓↓x = t␈↓ in some interpretation and ␈↓↓freefor(x,t,e)␈↓, then ␈↓↓subst(t,x,e) = t␈↓ in that interpretation.